|
SKI combinator calculus is a computational system that may be perceived as a reduced version of untyped lambda calculus. It can be thought of as a computer programming language, though it is not useful for writing software. Instead, it is important in the mathematical theory of algorithms because it is an extremely simple Turing complete language. All operations in lambda calculus are expressed in SKI as binary trees whose leaves are one of the three symbols S, K, and I (called ''combinators''). In fact, the symbol I is added only for convenience, and just the other two suffice for all of the purposes of the SKI system. Although the most formal representation of the objects in this system requires binary trees, they are usually represented, for typesetability, as parenthesized expressions, either with all the subtrees parenthesized, or only the right-side children subtrees parenthesized. So, the tree whose left subtree is the tree KS and whose right subtree is the tree SK is usually typed as ((KS)(SK)), or more simply as KS(SK), instead of being fully drawn as a tree (as formality and readability would require). ==Informal description== Informally, and using programming language jargon, a tree (''xy'') can be thought of as a "function" ''x'' applied to an "argument" ''y''. When "evaluated" (''i.e.'', when the function is "applied" to the argument), the tree "returns a value", ''i.e.'', transforms into another tree. Of course, all three of the "function", the "argument" and the "value" are either combinators, or binary trees, and if they are binary trees they too may be thought of as functions whenever the need arises. The evaluation operation is defined as follows: (''x'', ''y'', and ''z'' represent expressions made from the functions S, K, and I, and set values): I returns its argument: :I''x'' = ''x'' K, when applied to any argument ''x'', yields a one-argument constant function K''x'' , which, when applied to any argument, returns ''x'': :K''xy'' = ''x'' S is a substitution operator. It takes three arguments and then returns the first argument applied to the third, which is then applied to the result of the second argument applied to the third. More clearly: :S''xyz'' = ''xz''(''yz'') Example computation: SKSK evaluates to KK(SK) by the S-rule. Then if we evaluate KK(SK), we get K by the K-rule. As no further rule can be applied, the computation halts here. Note that, for all trees ''x'' and all trees ''y'', SK''xy'' will always evaluate to ''y'' in two steps, K''y''(''xy'') = ''y'', so the ultimate result of evaluating SK''xy'' will always equal the result of evaluating ''y''. We say that SK''x'' and I are "functionally equivalent" because they always yield the same result when applied to any ''y''. Note that from these definitions it can be shown that SKI calculus is not the minimum system that can fully perform the computations of lambda calculus, as all occurrences of I in any expression can be replaced by (SKK) or (SKS) or (SK whatever) and the resulting expression will yield the same result. So the "I" is merely syntactic sugar. In fact, it is possible to define a complete system using only one combinator. An example is Chris Barker's iota combinator, which can be expressed in terms of S and K as follows: : ι''x'' = ''x''SK It is possible to reconstruct S, K, and I from the iota combinator. Applying ι to itself gives ιι = ιSK = SSKK = SK(KK) which is functionally equivalent to I. K can be constructed by applying ι twice to I (which is equivalent to application of ι to itself): ι(ι(ιι)) = ι(ιI) yields ι(ISK) = ι(SK) = SKSK = K (see Example computation). Applying ι one more time gives ι(ι(ι(ιι))) = ιK = KSK = S. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「SKI combinator calculus」の詳細全文を読む スポンサード リンク
|